/*
 * SplittingTree.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef SPLITTINGTREE_HPP_
#define SPLITTINGTREE_HPP_

#include <utility>
#include <queue>

#include "bfr/ClauseSet.hpp"
#include "bfr/CoefficientType.hpp"

#include "bfr/lpbCombinatorial/SplittingTreeNode.hpp"
#include "bfr/lpbCombinatorial/VariableSetting.hpp"
#include "bfr/lpbCombinatorial/TreeContext.hpp"
#include "bfr/lpbCombinatorial/SolverInformation.hpp"

namespace bfr {

// forward declare SolverInformation and CoefficientChooser class
class SolverInformation;

/**
 * This class represents the whole splitting tree for a DNF.
 */
class SplittingTree {
    public:
        /**
         * Constructor.
         *
         * Creates a new tree given a DNF, an occurrence pattern factory
         * and the number of variables in the DNF.
         *
         * @param dnf The DNF of the root node \f$\phi\f$.
         * @param variableCount Number of variables in the DNF. If set to
         * -1 (default) it will calculate this value from the DNF.
         */
        SplittingTree(ClauseSet *dnf, size_t variableCount=-1);

        /**
         * Destructor.
         *
         * Will delete
         * <ul>
         *  <li>The VariableSetting</li>
         *  <li>All nodes in the tree</li>
         *  <li>The TreeContext</li>
         * </ul>
         *
         * Again note that the DNF of the root will not be destroyed,
         * see SplittingTreeNode#~SplittingTreeNode.
         *
         * @see SplittingTreeNode#~SplittingTreeNode
         */
        ~SplittingTree();

        /**
         * Create the complete tree.
         *
         * This method will call SplittingTreeNode#split
         * for all non-final nodes. It will recursively
         * create the whole tree.
         *
         * @param symmTest If this value is <code>true</code> a symmetry
         * test should be performed to check if the DNF fulfills the
         * symmetry property (see
         * <a href="http://www.informatik.uni-freiburg.de/~ki/papers/smaus-tr230.pdf">
         * Smaus 2007)
         * </a>. BIG TODO: how often is it necessary to do this? And we
         * actually ignore the variable.
         * @param deleteContent If set to <code>true</code> the content of all generated
         * SplittingTreeNode objects will be destroyed by calling
         * SplittingTreeNode#destroyContent (this will <b>NOT</b> destroy
         * the DNF of the root) neither the nodes itself, only the DNFs and
         * occurrence patterns to save memory.
         */
        template<bool Cut>
        void createTree(bool symmTest=false,
                bool deleteContent=true) {
	  //std::cout << "call createTree" << std::endl;
            std::queue<SplittingTreeNode*> waiting;
            waiting.push(root);

            while (!waiting.empty()) {
	      //std::cout << "entered while loop" << std::endl;
                SplittingTreeNode *next = waiting.front();
		//std::cout << *(next->getDNF()) << std::endl;
                waiting.pop();
	        //std::cout << "pop successful" << std::endl;
                if (next->isFinal() || next->isAlreadySplit()) {
		  //std::cout << "continue" << std::endl;
                    continue;
                }
		//std::cout << "before split" << std::endl;
                next->split<Cut>(vs, symmTest);
		//std::cout << "before split" << std::endl;
                if (deleteContent) {
                    next->destroyContent();
                } 
		//std::cout << "just before creating the children" << std::endl;
                SplittingTreeNode *child1 = next->getUpperChild();
                SplittingTreeNode *child2 = next->getLowerChild();
                // TODO add isFinal here again?
                if ((child1 != 0) && (!child1->isAlreadySplit())) {
                    waiting.push(child1);
                }

                if ((child2 != 0) && (!child2->isAlreadySplit())) {
                    waiting.push(child2);
                }
            }
	    //std::cout << "finish createTree" << std::endl;
        }

        /**
         * Return a pointer to the root node.
         *
         * @return Pointer to the root node.
         */
        SplittingTreeNode *getRoot() const;

        /**
         * Return the TreeContext.
         *
         * All nodes in the tree will share this context.
         *
         * @return Context of the tree.
         */
        TreeContext *getContext() const;

        /**
         * Return the variable setting of this tree.
         *
         * @return Variable setting that is used for this tree.
         */
        VariableSetting *getVariableSetting() const;

        /**
         * Return the number of columns in the tree.
         *
         * @return Number of columns.
         */
        size_t size() const;

        /**
         * Returns the number of final nodes in the complete tree.
         *
         * This method iterates over all node entries.
         *
         * @return Number of final nodes in the tree.
         */
        size_t numFinalNodes() const;

        /**
         * Returns the number of final true nodes in the complete tree.
         */
        size_t numFinalTrueNodes() const;

        /**
         * Returns the node that caused the min value in the last call
         * of handleColumn().
         */
        SplittingTreeNode *getMinCulprit() const;

        /**
         * Returns the node that caused the max value in the last call
         * of handleColumn().
         */
        SplittingTreeNode *getMaxCulprit() const;


        // TODO document me
        // actually the second definition doesn't work?... typename
        // is only allowed in a template context
        template<class CoefficientChooserT>
        std::pair<lpb_coefficient_t, lpb_coefficient_t> handleColumn(
                //SolverInformation::interval_t handleColumn(
                size_t column,
                const CoefficientChooserT &chooser,
                SolverInformation &information) {
                SplittingTreeNode *last = NULL;
                interval_t lastInterval, currentInterval;
                lpb_coefficient_t minSoFar = coeff_pos_infinity;
                lpb_coefficient_t maxSoFar = coeff_neg_infinity;
                // TODO: right?
                TreeContext::const_col_iterator col_begin =
                        context->columnBegin(column);
                minCulprit = *col_begin;
                maxCulprit = *col_begin;
                lpb_coefficient_t sum = information.getSumFrom(column + 1);
                size_t treeSize = size();
                // TODO change this to the faster method in the
                // SolverInformation class
                /*lpb_coefficient_t sum = 0;
                for (size_t i = column + 1; i < treeSize; i++) {
                    sum += information.getCoefficient(i);
                }*/
                TreeContext::const_col_iterator colEnd =
                        context->columnEnd(column);
                for (TreeContext::const_col_iterator it = col_begin;
                        it != colEnd;
                        it++) {
		  //std::cout << "next node in column ";
                    SplittingTreeNode *n = *it;
                    if (n->isFinal()) {
                        // DNF is either true or false
                        if (getDNFValue(n->getDNF())) {
                            // it represents true
			    //std::cout << " true" << std::endl;
                            information.setInterval(*n, coeff_neg_infinity, 0);
                            currentInterval.first = coeff_neg_infinity;
                            currentInterval.second = 0;
                        }
                        else {
                            // it represents false
			    //std::cout << " false" << std::endl;
                            information.setInterval(*n, sum, coeff_pos_infinity);
                            currentInterval.first = sum;
                            currentInterval.second = coeff_pos_infinity;
                        }
                    }
                    else {
                        // not a final node
                        lpb_coefficient_t s0, s1, b0, b1, s, b;
                        interval_t upper, lower;
                        if (n->getUpperChild() == 0) {
                            // dnf is false
                            assert(n->getDNF()->size() == 0);
                            information.setInterval(*n, sum, coeff_pos_infinity);
                            currentInterval.first = sum;
                            currentInterval.second = coeff_pos_infinity;
                            assert(n->getLowerChild() != 0);
                            lower = information.getInterval(*(n->getLowerChild()));
                            upper = interval_t(sum - information.getCoefficient(treeSize - 1),
                                    coeff_pos_infinity);
                        }
                        else if (n->getLowerChild() == 0) {
                            // it represents true
                            #ifndef NDEBUG
                            assert(n->getDNF()->size() == 1);
                            const Clause *clause = *(n->getDNF()->begin());
                            assert(clause->size() == 0);
                            #endif // NDEBUG
                            information.setInterval(*n, coeff_neg_infinity, 0);
                            currentInterval.first = coeff_neg_infinity;
                            currentInterval.second = 0;
                            assert(n->getUpperChild() != 0);
                            upper = information.getInterval(*(n->getUpperChild()));
                            lower = interval_t(coeff_neg_infinity, 0);
                        }
                        else {
                            upper = information.getInterval(*(n->getUpperChild()));
                            lower = information.getInterval(*(n->getLowerChild()));
                        }
                        s0 = upper.first;
                        b0 = upper.second;
                        s1 = lower.first;
                        b1 = lower.second;
                        const lpb_coefficient_t coeff =
                                information.getCoefficient(column + 1);

                        s = std::max(s0, s1 + coeff);
                        b = std::min(b0, b1 + coeff);
                        information.setInterval(*n, s, b);
                        currentInterval.first = s;
                        currentInterval.second = b;
                    }

                    // should work so?
                    if ((last != 0) && (n->getUpperParent() != 0) 
			&& n->getUpperParent()->getUpperChild() != 0) {//JGS: was commented out
                        const lpb_coefficient_t dif1 = lastInterval.first -
                                currentInterval.second;
                        const lpb_coefficient_t dif2 = lastInterval.second -
                                currentInterval.first;
			//std::cout << "lb = " << dif1 << std::endl;
			//std::cout << "ub = " << dif2 << std::endl;

                        if (dif1 > maxSoFar) {
                            maxSoFar = dif1;
                            maxCulprit = last;
			    information.setMaxCulprit(column, last);
			    information.setLowerComputedBound(column, dif1);
                        }

                        if (dif2 < minSoFar) {
                            minSoFar = dif2;
                            minCulprit = last;
			    information.setMinCulprit(column, last);
			    information.setUpperComputedBound(column, dif2);
                        }
                    }
                    last = n;
                    lastInterval = currentInterval;
                }
                // check if we have an integer conflict
                return interval_t(maxSoFar, minSoFar);
        }

    private:
        SplittingTreeNode *root;
        VariableSetting *vs;
        TreeContext *context;

        // Initialized to NULL but after calling handleColumn this node
        // is the upper node that caused the minimum
        SplittingTreeNode *minCulprit;
        // Initialized to NULL but after calling handleColumn this node
        // is the upper node that caused the maximum
        SplittingTreeNode *maxCulprit;

    protected:

        /**
         * Check if a DNF represents <i>true</i> or <i>false</i>.
         *
         * This method checks for a given DNF if it
         * represents <i>true</i> or <i>false</i>.
         *
         * This method should only be used if you know that the DNF
         * is <i>true</i> or <i>false</i>, otherwise this method
         * does not make sense.
         *
         * @param dnf The DNF to check.
         *
         * @return <code>true</code> if the DNF represents <i>true</i>.
         */
        bool getDNFValue(ClauseSet *dnf) const;
};

}

#endif  // SPLITTINGTREE_HPP_
